M:MsgA, k:Knd, l:IdLnk. M.bframe(k sends on l)  Prop 

latex

Definitions	Knd, t  T, IdLnk, type List, x.A(x), x:A. B(x), x. t(x), Top, a:A fp B(a), x:AB(x), KindDeq, x  dom(f), b, Type, {x:A| B(x) }, IdLnkDeq, deq-member(eq;x;L), Prop, x,y. t(x;y), z != f(x)  P(a;z), M.bframe(k sends on l), x:AB(x), MsgA
Lemmas	msga wf, fpf-val wf, deq-member wf, idlnk-deq wf, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, IdLnk wf, Knd wf